TypeNames:Type, d:DS(TypeNames), a:TypeNames.
dseq(d;a)  dstype(TypeNames; d; a)dstype(TypeNames; d; a) 

latex

Definitions	x:A. B(x), DS(A), t  T, dstype(TypeNames; d; a), dseq(d;a), x. t(x), x(s)
Lemmas	eqof wf, pi1 wf, deq wf, pi2 wf